MatchIrrelevant.agda:21,8-12
Cannot pattern match against irrelevant argument of type NAT zero
when checking that the pattern Zero has type NAT zero
